$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$x$:$T$. Dec($P$($x$))) $\Rightarrow$ (finite{-}type(\{$x$:$T$$\mid$ $P$($x$)\} ) $\Leftarrow\!\Rightarrow$ ($\exists$$L$:$T$ List. ($\forall$$x$:$T$. $P$($x$) $\Rightarrow$ ($x$ $\in$ $L$))))